В табл. 7.2 воспроизведен в более точной форме процесс формирования рассуждений, который проиллюстрирован на рис. 7.4. Общий алгоритм определения логического следствия в пропозициональной логике приведен в листинге 7.3. Как и в алгоритме Backtracking-Search, приведенном на с. 131, функция TT-Entails? осуществляет рекурсивный перебор конечного пространства вариантов присваивания значений переменным. Этот алгоритм является непротиворечивым, поскольку он непосредственно реализует определение логического следствия, и полным, поскольку может применяться для любой базы знаний KB и любого высказывания а и всегда заканчивает свою работу, при условии, что количество моделей, подлежащих проверке, является конечным.

Листинг 7.3. Алгоритм перебора истинностной таблицы для получения пропозициональных логических следствий, тт обозначает истинностную таблицу, функция PL-True? возвращает истинное значение, если некоторое высказывание является истинным в рамках некоторой модели. Переменная model представляет частично заданную модель — присваивание только некоторым переменным. Вызов функции Extend(Р, true,model) возвращает новую частично заданную модель, в которой высказывание Р имеет значение true

Безусловно, выражение "является конечным" не всегда означает то же, что и выражение "является небольшим". Если KB и а содержат в целом п символов, то количество моделей равно. Таким образом, временная сложность этого алгоритма составляет. (Пространственная сложность составляет только О(п), поскольку перебор вариантов присваивания происходит по принципу поиска в глубину.) Ниже будут показаны алгоритмы, которые являются гораздо более эффективными на практике. К сожалению, каждый известный алгоритм логического вывода для пропозициональной логики в худшем случае имеет сложность, экспоненциально зависящую от размера ввода. Мы не можем рассчитывать на то, что наши алгоритмы будут действовать лучше, поскольку задача получения пропозиционального логического следствия является ko-NP-полной (см. приложение А).